SherbyNet - /page/wikibook/entry.mu

<!DOCTYPE html>

<title>Quantifier elimination</title>

</head>

Quantifier elimination

</h1>

</header>

Quantifier elimination is a concept of simplification used in <a href="Mathematical_logic" title="Mathematical logic">mathematical logic</a>, <a href="Model_theory" title="Model theory">model theory</a>, and <a href="Theoretical_computer_science" title="Theoretical computer science">theoretical computer science</a>. Informally, a quantified statement "<math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \exists x}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \exists x}</annotation>

</semantics>

</math><img src="./ab833914405cde960b3b9af3feaa9e4fef96ffa9.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.622ex; height:2.176ex;" alt="{\displaystyle \exists x}" loading="lazy"> such that ..." can be viewed as a question "When is there an <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle x}</annotation>

</semantics>

</math><img src="./87f9e315fd7e2ba406057a97300593c4802b53e4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.33ex; height:1.676ex;" alt="{\displaystyle x}" loading="lazy"> such that ...?", and the statement without quantifiers can be viewed as the answer to that question.<a href="#cite_note-FOOTNOTEBrown2002-1">[1]</a>

One way of classifying <a href="Well-formed_formula" title="Well-formed formula">formulas</a> is by the amount of <a href="Quantifier_(logic)" title="Quantifier (logic)">quantification</a>. Formulas with less <a href="Quantifier_(logic)#Nesting" title="Quantifier (logic)">depth of quantifier alternation</a> are thought of as being simpler, with the quantifier-free formulas as the simplest.

A <a href="Logical_theory" class="mw-redirect" title="Logical theory">theory</a> has quantifier elimination if for every formula <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \alpha }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \alpha }</annotation>

</semantics>

</math><img src="./b79333175c8b3f0840bfb4ec41b8072c83ea88d3.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.488ex; height:1.676ex;" alt="{\displaystyle \alpha }" loading="lazy">, there exists another formula <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \alpha _{QF}}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \alpha _{QF}}</annotation>

</semantics>

</math><img src="./e8e52ee8fb776f7c919339cfc8eab2006b3f1e6c.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:4.251ex; height:2.343ex;" alt="{\displaystyle \alpha _{QF}}" loading="lazy"> without quantifiers that is <a href="Logical_equivalence" title="Logical equivalence">equivalent</a> to it (<a href="Modulo_(jargon)" class="mw-redirect" title="Modulo (jargon)">modulo</a> this theory).

<div class="mw-heading mw-heading2"><h2 id="Examples">Examples</h2></div>

An example from mathematics says that a single-variable <a href="Quadratic_polynomial" class="mw-redirect" title="Quadratic polynomial">quadratic polynomial</a> has a real root if and only if its <a href="Discriminant" title="Discriminant">discriminant</a> is non-negative:<a href="#cite_note-FOOTNOTEBrown2002-1">[1]</a>

</mrow>

<msup>

</mrow>

</msup>

<msup>

</mrow>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \exists x\in \mathbb {R} .(a\neq 0\wedge ax^{2}+bx+c=0)\ \ \Longleftrightarrow \ \ a\neq 0\wedge b^{2}-4ac\geq 0}</annotation>

</semantics>

</math>

Here the sentence on the left-hand side involves a quantifier <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \exists x\in \mathbb {R} }">

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \exists x\in \mathbb {R} }</annotation>

</semantics>

</math><img src="./be0e857feee05b3e653596f886aba41280fb235e.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:7.141ex; height:2.176ex;" alt="{\displaystyle \exists x\in \mathbb {R} }" loading="lazy">, whereas the equivalent sentence on the right does not.

Examples of theories that have been shown decidable using quantifier elimination are <a href="Presburger_arithmetic" title="Presburger arithmetic">Presburger arithmetic</a>,<a href="#cite_note-FOOTNOTEPresburger1929-2">[2]</a><a href="#cite_note-3">[3]</a><a href="#cite_note-4">[4]</a><a href="#cite_note-FOOTNOTEMonk2012240-5">[5]</a><a href="#cite_note-FOOTNOTEEnderton2001188-6">[6]</a> <a href="Algebraically_closed_field" title="Algebraically closed field">algebraically closed fields</a>, <a href="Real_closed_field" title="Real closed field">real closed fields</a>,<a href="#cite_note-FOOTNOTEGrädel_et_al.2007-7">[7]</a><a href="#cite_note-FOOTNOTEFriedJarden2008171-8">[8]</a> <a href="Atom_(order_theory)" title="Atom (order theory)">atomless</a> <a href="Boolean_algebras" class="mw-redirect" title="Boolean algebras">Boolean algebras</a>, <a href="Term_algebra" title="Term algebra">term algebras</a>, <a href="Dense_linear_order" class="mw-redirect" title="Dense linear order">dense linear orders</a>,<a href="#cite_note-FOOTNOTEGrädel_et_al.2007-7">[7]</a> <a href="Abelian_group" title="Abelian group">abelian groups</a>,<a href="#cite_note-FOOTNOTESzmielew1955Page_229_describes_"the_method_of_eliminating_quantification".-9">[9]</a> <a href="Random_graph" title="Random graph">random graphs</a>, as well as many of their combinations such as Boolean algebra with Presburger arithmetic, and term algebras with <a href="Queue_(mathematics)" class="mw-redirect" title="Queue (mathematics)">queues</a>.

Quantifier elimination for the theory of the real numbers as an <a href="Ordered_group" class="mw-redirect" title="Ordered group">ordered additive group</a> is <a href="Fourier%E2%80%93Motzkin_elimination" title="Fourier–Motzkin elimination">Fourier–Motzkin elimination</a>; for the theory of the field of real numbers it is the <a href="Tarski%E2%80%93Seidenberg_theorem" title="Tarski–Seidenberg theorem">Tarski–Seidenberg theorem</a>.<a href="#cite_note-FOOTNOTEGrädel_et_al.2007-7">[7]</a>

Quantifier elimination can also be used to show that "combining" <a href="Decidability_(logic)" title="Decidability (logic)">decidable</a> theories leads to new decidable theories (see <a href="Feferman%E2%80%93Vaught_theorem" title="Feferman–Vaught theorem">Feferman–Vaught theorem</a>).

<div class="mw-heading mw-heading2"><h2 id="Algorithms_and_decidability">Algorithms and decidability</h2></div>

If a theory has quantifier elimination, then a specific question can be addressed: Is there a method of determining <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \alpha _{QF}}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \alpha _{QF}}</annotation>

</semantics>

</math><img src="./e8e52ee8fb776f7c919339cfc8eab2006b3f1e6c.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:4.251ex; height:2.343ex;" alt="{\displaystyle \alpha _{QF}}" loading="lazy"> for each <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \alpha }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \alpha }</annotation>

</semantics>

</math><img src="./b79333175c8b3f0840bfb4ec41b8072c83ea88d3.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.488ex; height:1.676ex;" alt="{\displaystyle \alpha }" loading="lazy">? If there is such a method we call it a quantifier elimination <a href="Algorithm" title="Algorithm">algorithm</a>. If there is such an algorithm, then <a href="Decidability_(logic)#Decidability_of_a_theory" title="Decidability (logic)">decidability</a> for the theory reduces to deciding the truth of the quantifier-free <a href="Sentence_(mathematical_logic)" title="Sentence (mathematical logic)">sentences</a>. Quantifier-free sentences have no variables, so their validity in a given theory can often be computed, which enables the use of quantifier elimination algorithms to decide validity of sentences.

<div class="mw-heading mw-heading2"><h2 id="Related_concepts">Related concepts</h2></div>

Various model-theoretic ideas are related to quantifier elimination, and there are various equivalent conditions.

Every <a href="First-order_logic" title="First-order logic">first-order</a> theory with quantifier elimination is <a href="Model_complete" class="mw-redirect" title="Model complete">model complete</a>. Conversely, a model-complete theory, whose theory of universal consequences has the <a href="Amalgamation_property" title="Amalgamation property">amalgamation property</a>, has quantifier elimination.<a href="#cite_note-FOOTNOTEHodges1993-10">[10]</a>

The models of the theory of the universal consequences of a theory <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle T}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle T}</annotation>

</semantics>

</math><img src="./ec7200acd984a1d3a3d7dc455e262fbe54f7f6e0.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.636ex; height:2.176ex;" alt="{\displaystyle T}" loading="lazy"> are precisely the <a href="Substructure_(mathematics)" title="Substructure (mathematics)">substructures</a> of the models of <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle T}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle T}</annotation>

</semantics>

</math><img src="./ec7200acd984a1d3a3d7dc455e262fbe54f7f6e0.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.636ex; height:2.176ex;" alt="{\displaystyle T}" loading="lazy">.<a href="#cite_note-FOOTNOTEHodges1993-10">[10]</a> The theory of linear orders does not have quantifier elimination. However the theory of its universal consequences has the amalgamation property.

<div class="mw-heading mw-heading2"><h2 id="Basic_ideas">Basic ideas</h2></div>

To show constructively that a theory has quantifier elimination, it suffices to show that we can eliminate an <a href="Existential_quantifier" class="mw-redirect" title="Existential quantifier">existential quantifier</a> applied to a conjunction of <a href="Literal_(mathematical_logic)" title="Literal (mathematical logic)">literals</a>, that is, show that each formula of the form:

</mrow>

</mrow>

</munderover>

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \exists x.\bigwedge _{i=1}^{n}L_{i}}</annotation>

</semantics>

</math>

where each <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle L_{i}}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle L_{i}}</annotation>

</semantics>

</math><img src="./fbbedf9f5f71ca52f8f24392c3cc18fca6c420dc.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.383ex; height:2.509ex;" alt="{\displaystyle L_{i}}" loading="lazy"> is a literal, is equivalent to a quantifier-free formula. Indeed, suppose we know how to eliminate quantifiers from conjunctions of literals, then if <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle F}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle F}</annotation>

</semantics>

</math><img src="./545fd099af8541605f7ee55f08225526be88ce57.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.741ex; height:2.176ex;" alt="{\displaystyle F}" loading="lazy"> is a quantifier-free formula, we can write it in <a href="Disjunctive_normal_form" title="Disjunctive normal form">disjunctive normal form</a>

</mrow>

</mrow>

</munderover>

</mrow>

</mrow>

</munderover>

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \bigvee _{j=1}^{m}\bigwedge _{i=1}^{n}L_{ij},}</annotation>

</semantics>

</math>

and use the fact that

</mrow>

</mrow>

</munderover>

</mrow>

</mrow>

</munderover>

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \exists x.\bigvee _{j=1}^{m}\bigwedge _{i=1}^{n}L_{ij}}</annotation>

</semantics>

</math>

is equivalent to

</mrow>

</mrow>

</munderover>

</mrow>

</mrow>

</munderover>

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \bigvee _{j=1}^{m}\exists x.\bigwedge _{i=1}^{n}L_{ij}.}</annotation>

</semantics>

</math>

Finally, to eliminate a universal quantifier

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \forall x.F}</annotation>

</semantics>

</math>

where <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle F}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle F}</annotation>

</semantics>

</math><img src="./545fd099af8541605f7ee55f08225526be88ce57.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.741ex; height:2.176ex;" alt="{\displaystyle F}" loading="lazy"> is quantifier-free, we transform

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \lnot F}</annotation>

</semantics>

</math><img src="./d1be87d4b5b721f671dcfaba45472bea40ccd6c9.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:3.291ex; height:2.176ex;" alt="{\displaystyle \lnot F}" loading="lazy"> into disjunctive normal form, and use the fact that <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \forall x.F}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \forall x.F}</annotation>

</semantics>

</math><img src="./585f18ba5664a870b7e0900e6cd340767dfb73d9.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:5.397ex; height:2.176ex;" alt="{\displaystyle \forall x.F}" loading="lazy">

is equivalent to <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \lnot \exists x.\lnot F.}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \lnot \exists x.\lnot F.}</annotation>

</semantics>

</math><img src="./ba39e0f65aa3aec3b4fea6aa4aabba5a5e8424b8.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:9.144ex; height:2.176ex;" alt="{\displaystyle \lnot \exists x.\lnot F.}" loading="lazy">

<div class="mw-heading mw-heading2"><h2 id="Relationship_with_decidability">Relationship with decidability</h2></div>

In early model theory, quantifier elimination was used to demonstrate that various theories possess properties like <a href="Decidability_(logic)" title="Decidability (logic)">decidability</a> and <a href="Complete_theory" title="Complete theory">completeness</a>. A common technique was to show first that a theory admits elimination of quantifiers and thereafter prove decidability or completeness by considering only the quantifier-free formulas. This technique can be used to show that <a href="Presburger_arithmetic" title="Presburger arithmetic">Presburger arithmetic</a> is decidable.

Theories could be decidable yet not admit quantifier elimination. Strictly speaking, the theory of the additive natural numbers did not admit quantifier elimination, but it was an expansion of the additive natural numbers that was shown to be decidable. Whenever a theory is decidable, and the <a href="Formal_language" title="Formal language">language</a> of its valid formulas is <a href="Countable" class="mw-redirect" title="Countable">countable</a>, it is possible to extend the theory with countably many <a href="Relation_(mathematics)" title="Relation (mathematics)">relations</a> to have quantifier elimination (for example, one can introduce, for each formula of the theory, a relation symbol that relates the <a href="Free_variable" class="mw-redirect" title="Free variable">free variables</a> of the formula).

Example: <a href="Nullstellensatz" class="mw-redirect" title="Nullstellensatz">Nullstellensatz</a> for <a href="Algebraically_closed_field" title="Algebraically closed field">algebraically closed fields</a> and for <a href="Differentially_closed_field" title="Differentially closed field">differentially closed fields</a>.

<ul><li><a href="Cylindrical_algebraic_decomposition" title="Cylindrical algebraic decomposition">Cylindrical algebraic decomposition</a></li>

<li><a href="Elimination_theory" title="Elimination theory">Elimination theory</a></li>

<li><a href="Conjunction_elimination" title="Conjunction elimination">Conjunction elimination</a></li></ul>

<div class="mw-heading mw-heading2"><h2 id="Notes">Notes</h2></div>

/* start https://en.wikipedia.org/ */

.mw-parser-output .reflist{margin-bottom:0.5em;list-style-type:decimal}@media screen{.mw-parser-output .reflist{font-size:90%}}.mw-parser-output .reflist .references{font-size:100%;margin-bottom:0;list-style-type:inherit}.mw-parser-output .reflist-columns-2{column-width:30em}.mw-parser-output .reflist-columns-3{column-width:25em}.mw-parser-output .reflist-columns{margin-top:0.3em}.mw-parser-output .reflist-columns ol{margin-top:0}.mw-parser-output .reflist-columns li{page-break-inside:avoid;break-inside:avoid-column}.mw-parser-output .reflist-upper-alpha{list-style-type:upper-alpha}.mw-parser-output .reflist-upper-roman{list-style-type:upper-roman}.mw-parser-output .reflist-lower-alpha{list-style-type:lower-alpha}.mw-parser-output .reflist-lower-greek{list-style-type:lower-greek}.mw-parser-output .reflist-lower-roman{list-style-type:lower-roman}

/* end https://en.wikipedia.org/ */

</style><div class="reflist reflist-columns references-column-width">

<li id="cite_note-FOOTNOTEBrown2002-1">^ <a href="#cite_ref-FOOTNOTEBrown2002_1-0">a</a> <a href="#cite_ref-FOOTNOTEBrown2002_1-1">b</a> <a href="#CITEREFBrown2002">Brown 2002</a>.

</li>

<li id="cite_note-FOOTNOTEPresburger1929-2"><a href="#cite_ref-FOOTNOTEPresburger1929_2-0">^</a> <a href="#CITEREFPresburger1929">Presburger 1929</a>.

</li>

<li id="cite_note-3"><a href="#cite_ref-3">^</a> Mind: basic <a href="Presburger_arithmetic" title="Presburger arithmetic">Presburger arithmetic</a> — <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \langle \mathbb {N} ,+,0,1\rangle }">

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \langle \mathbb {N} ,+,0,1\rangle }</annotation>

</semantics>

</math><img src="./12a8bc5df07665e71e3b22c0b1ad7d0bbd60f504.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:10.722ex; height:2.843ex;" alt="{\displaystyle \langle \mathbb {N} ,+,0,1\rangle }" loading="lazy"> — does not admit quantifier elimination. <a href="#CITEREFNipkow2010">Nipkow (2010)</a>: "Presburger arithmetic needs a divisibility (or congruence) predicate '|' to allow quantifier elimination".

</li>

<li id="cite_note-4"><a href="#cite_ref-4">^</a> <a href="#CITEREFGrädel_et_al.2007">Grädel et al. (2007</a>, p. 20) define <a href="Presburger_arithmetic" title="Presburger arithmetic">Presburger arithmetic</a> as <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \langle \mathbb {N} ,+,<,0,1,(\equiv _{k})_{k>0}\rangle {\text{ where }}x\equiv _{k}y{\text{ iff }}x=y(\mod {k})}">

</mrow>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<mtext> where </mtext>

</mrow>

<msub>

</mrow>

</msub>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \langle \mathbb {N} ,+,<,0,1,(\equiv _{k})_{k>0}\rangle {\text{ where }}x\equiv _{k}y{\text{ iff }}x=y(\mod {k})}</annotation>

</semantics>

</math><img src="./a78b66a25ade3ea9e3723a399ea8dbe903cd8d0b.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:55.985ex; height:2.843ex;" alt="{\displaystyle \langle \mathbb {N} ,+,<,0,1,(\equiv _{k})_{k>0}\rangle {\text{ where }}x\equiv _{k}y{\text{ iff }}x=y(\mod {k})}" loading="lazy">. This extension does admit quantifier elimination.

</li>

<li id="cite_note-FOOTNOTEMonk2012240-5"><a href="#cite_ref-FOOTNOTEMonk2012240_5-0">^</a> <a href="#CITEREFMonk2012">Monk 2012</a>, p. 240.

</li>

<li id="cite_note-FOOTNOTEEnderton2001188-6"><a href="#cite_ref-FOOTNOTEEnderton2001188_6-0">^</a> <a href="#CITEREFEnderton2001">Enderton 2001</a>, p. 188.

</li>

<li id="cite_note-FOOTNOTEGrädel_et_al.2007-7">^ <a href="#cite_ref-FOOTNOTEGrädel_et_al.2007_7-0">a</a> <a href="#cite_ref-FOOTNOTEGrädel_et_al.2007_7-1">b</a> <a href="#cite_ref-FOOTNOTEGrädel_et_al.2007_7-2">c</a> <a href="#CITEREFGrädel_et_al.2007">Grädel et al. 2007</a>.

</li>

<li id="cite_note-FOOTNOTEFriedJarden2008171-8"><a href="#cite_ref-FOOTNOTEFriedJarden2008171_8-0">^</a> <a href="#CITEREFFriedJarden2008">Fried & Jarden 2008</a>, p. 171.

</li>

<li id="cite_note-FOOTNOTESzmielew1955Page_229_describes_"the_method_of_eliminating_quantification".-9"><a href="#cite_ref-FOOTNOTESzmielew1955Page_229_describes_"the_method_of_eliminating_quantification"._9-0">^</a> <a href="#CITEREFSzmielew1955">Szmielew 1955</a>, Page 229 describes "the method of eliminating quantification"..

</li>

<li id="cite_note-FOOTNOTEHodges1993-10">^ <a href="#cite_ref-FOOTNOTEHodges1993_10-0">a</a> <a href="#cite_ref-FOOTNOTEHodges1993_10-1">b</a> <a href="#CITEREFHodges1993">Hodges 1993</a>.

</li>

</ol></div>

<div class="mw-heading mw-heading2"><h2 id="References">References</h2></div>

/* start https://en.wikipedia.org/ */

.mw-parser-output .refbegin{margin-bottom:0.5em}.mw-parser-output .refbegin-hanging-indents>ul{margin-left:0}.mw-parser-output .refbegin-hanging-indents>ul>li{margin-left:0;padding-left:3.2em;text-indent:-3.2em}.mw-parser-output .refbegin-hanging-indents ul,.mw-parser-output .refbegin-hanging-indents ul li{list-style:none}@media(max-width:720px){.mw-parser-output .refbegin-hanging-indents>ul>li{padding-left:1.6em;text-indent:-1.6em}}.mw-parser-output .refbegin-columns{margin-top:0.3em}.mw-parser-output .refbegin-columns ul{margin-top:0}.mw-parser-output .refbegin-columns li{page-break-inside:avoid;break-inside:avoid-column}@media screen{.mw-parser-output .refbegin{font-size:90%}}

/* end https://en.wikipedia.org/ */

</style><div class="refbegin" style="">

/* start https://en.wikipedia.org/ */

.mw-parser-output cite.citation{font-style:inherit;word-wrap:break-word}.mw-parser-output .citation q{quotes:"\"""\"""'""'"}.mw-parser-output .citation:target{background-color:rgba(0,127,255,0.133)}.mw-parser-output .id-lock-free.id-lock-free a{background:url("./mw/Lock-green.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-limited.id-lock-limited a,.mw-parser-output .id-lock-registration.id-lock-registration a{background:url("./mw/Lock-gray-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-subscription.id-lock-subscription a{background:url("./mw/Lock-red-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .cs1-ws-icon a{background:url("./mw/Wikisource-logo.svg")right 0.1em center/12px no-repeat}body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-free a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-limited a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-registration a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-subscription a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .cs1-ws-icon a{background-size:contain;padding:0 1em 0 0}.mw-parser-output .cs1-code{color:inherit;background:inherit;border:none;padding:inherit}.mw-parser-output .cs1-hidden-error{display:none;color:var(--color-error,#d33)}.mw-parser-output .cs1-visible-error{color:var(--color-error,#d33)}.mw-parser-output .cs1-maint{display:none;color:#085;margin-left:0.3em}.mw-parser-output .cs1-kern-left{padding-left:0.2em}.mw-parser-output .cs1-kern-right{padding-right:0.2em}.mw-parser-output .citation .mw-selflink{font-weight:inherit}@media screen{.mw-parser-output .cs1-format{font-size:95%}html.skin-theme-clientpref-night .mw-parser-output .cs1-maint{color:#18911f}}@media screen and (prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .cs1-maint{color:#18911f}}

/* end https://en.wikipedia.org/ */

</style><cite id="CITEREFBrown2002" class="citation web cs1">Brown, Christopher W. (July 31, 2002). <a rel="nofollow" class="external text" href="https://www.usna.edu/CS/qepcadweb/B/QE.html">"What is Quantifier Elimination"</a>. Retrieved 30 August 2023.</cite></li></ul>

<ul><li><cite id="CITEREFCooper1972" class="citation journal cs1">Cooper, D.C. (1972). <a href="Bernard_Meltzer_(computer_scientist)" title="Bernard Meltzer (computer scientist)">Meltzer, Bernard</a>; <a href="Donald_Michie" title="Donald Michie">Michie, Donald</a> (eds.). <a rel="nofollow" class="external text" href="https://www.cs.cmu.edu/~emc/spring06/home1_files/Cooper.pdf">"Theorem Proving in Arithmetic without Multiplication"</a> (PDF). Machine Intelligence. 7. Edinburgh: Edinburgh University Press: 91–99. Retrieved 30 August 2023.</cite></li></ul>

<ul><li><cite id="CITEREFEnderton2001" class="citation book cs1"><a href="Herbert_Enderton" title="Herbert Enderton">Enderton, Herbert</a> (2001). A mathematical introduction to logic (2nd ed.). Boston, MA: <a href="Academic_Press" title="Academic Press">Academic Press</a>. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-0-12-238452-3</bdi>.</cite></li></ul>

<ul><li><cite id="CITEREFFriedJarden2008" class="citation book cs1">Fried, Michael D.; Jarden, Moshe (2008). Field arithmetic. Ergebnisse der Mathematik und ihrer Grenzgebiete. 3. Folge. Vol. 11 (3rd revised ed.). <a href="Springer-Verlag" class="mw-redirect" title="Springer-Verlag">Springer-Verlag</a>. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-3-540-77269-9</bdi>. <a href="Zbl_(identifier)" class="mw-redirect" title="Zbl (identifier)">Zbl</a> <a rel="nofollow" class="external text" href="https://zbmath.org/?format=complete&q=an:1145.12001">1145.12001</a>.</cite></li></ul>

<ul><li><cite id="CITEREFGrädel_et_al.2007" class="citation book cs1">Grädel, Erich; <a href="Phokion_G._Kolaitis" title="Phokion G. Kolaitis">Kolaitis, Phokion G.</a>; <a href="Leonid_Libkin" title="Leonid Libkin">Libkin, Leonid</a>; Maarten, Marx; <a href="Joel_Spencer" title="Joel Spencer">Spencer, Joel</a>; <a href="Moshe_Y._Vardi" class="mw-redirect" title="Moshe Y. Vardi">Vardi, Moshe Y.</a>; Venema, Yde; Weinstein, Scott (2007). Finite model theory and its applications. Texts in Theoretical Computer Science. An EATCS Series. Berlin: <a href="Springer-Verlag" class="mw-redirect" title="Springer-Verlag">Springer-Verlag</a>. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-3-540-00428-8</bdi>. <a href="Zbl_(identifier)" class="mw-redirect" title="Zbl (identifier)">Zbl</a> <a rel="nofollow" class="external text" href="https://zbmath.org/?format=complete&q=an:1133.03001">1133.03001</a>.</cite></li></ul>

<ul><li><cite id="CITEREFHodges1993" class="citation book cs1"><a href="Wilfrid_Hodges" title="Wilfrid Hodges">Hodges, Wilfrid</a> (1993). Model Theory. Encyclopedia of Mathematics and its Applications. Vol. 42. <a href="Cambridge_University_Press" title="Cambridge University Press">Cambridge University Press</a>. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1017%2FCBO9780511551574">10.1017/CBO9780511551574</a>. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>9780521304429</bdi>.</cite></li></ul>

<ul><li><cite id="CITEREFKuncakRinard2003" class="citation book cs1">Kuncak, Viktor; Rinard, Martin (2003). <a rel="nofollow" class="external text" href="https://infoscience.epfl.ch/record/110222/files/KuncakRinard03StructuralSubtypingNonRecursiveTypesDecidable.pdf">"Structural subtyping of non-recursive types is decidable"</a> (PDF). 18th Annual IEEE Symposium of Logic in Computer Science, 2003. Proceedings. pp. 96–107. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1109%2FLICS.2003.1210049">10.1109/LICS.2003.1210049</a>. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>0-7695-1884-2</bdi>. <a href="S2CID_(identifier)" class="mw-redirect" title="S2CID (identifier)">S2CID</a> <a rel="nofollow" class="external text" href="https://api.semanticscholar.org/CorpusID:14182674">14182674</a>.</cite></li></ul>

<ul><li><cite id="CITEREFMonk2012" class="citation book cs1">Monk, J. Donald (2012). Mathematical Logic (Graduate Texts in Mathematics (37)) (Softcover reprint of the original 1st ed. 1976 ed.). Springer. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>9781468494549</bdi>.</cite></li></ul>

<ul><li><cite id="CITEREFNipkow2010" class="citation journal cs1"><a href="Tobias_Nipkow" title="Tobias Nipkow">Nipkow, Tobias</a> (2010). <a rel="nofollow" class="external text" href="https://www21.in.tum.de/~nipkow/pubs/ijcar08.pdf">"Linear Quantifier Elimination"</a> (PDF). <a href="Journal_of_Automated_Reasoning" title="Journal of Automated Reasoning">Journal of Automated Reasoning</a>. 45 (2): 189–212. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1007%2Fs10817-010-9183-0">10.1007/s10817-010-9183-0</a>. <a href="S2CID_(identifier)" class="mw-redirect" title="S2CID (identifier)">S2CID</a> <a rel="nofollow" class="external text" href="https://api.semanticscholar.org/CorpusID:14279141">14279141</a>. Retrieved 2022-11-12.</cite></li></ul>

<ul><li><cite id="CITEREFPresburger1929" class="citation journal cs1"><a href="Moj%C5%BCesz_Presburger" title="Mojżesz Presburger">Presburger, Mojżesz</a> (1929). "Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt". Comptes Rendus du I congrès de Mathématiciens des Pays Slaves, Warszawa: 92–101.</cite>, see <a href="#CITEREFStansifer1984">Stansifer (1984)</a> for an English translation</li></ul>

<ul><li><cite id="CITEREFStansifer1984" class="citation report cs1 cs1-prop-long-vol">Stansifer, Ryan (Sep 1984). <a rel="nofollow" class="external text" href="http://cs.fit.edu/~ryan/papers/presburger.pdf">Presburger's Article on Integer Arithmetic: Remarks and Translation</a> (PDF) (Technical Report). Vol. TR84-639. Ithaca, New York: Dept. of Computer Science, Cornell University.</cite></li></ul>

<ul><li><cite id="CITEREFSzmielew1955" class="citation journal cs1"><a href="Wanda_Szmielew" title="Wanda Szmielew">Szmielew, Wanda</a> (1955). <a rel="nofollow" class="external text" href="https://doi.org/10.4064%2Ffm-41-2-203-271">"Elementary properties of Abelian groups"</a>. <a href="Fundamenta_Mathematicae" title="Fundamenta Mathematicae">Fundamenta Mathematicae</a>. 41 (2): 203–271. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.4064%2Ffm-41-2-203-271">10.4064/fm-41-2-203-271</a>. <a href="MR_(identifier)" class="mw-redirect" title="MR (identifier)">MR</a> <a rel="nofollow" class="external text" href="https://mathscinet.ams.org/mathscinet-getitem?mr=0072131">0072131</a>.</cite></li></ul>

<ul><li><cite id="CITEREFJeannerodTreinen" class="citation conference cs1">Jeannerod, Nicolas; Treinen, Ralf. Deciding the First-Order Theory of an Algebra of Feature Trees with Updates. International Joint Conference on Automated Reasoning (IJCAR). <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1007%2F978-3-319-94205-6_29">10.1007/978-3-319-94205-6_29</a>.</cite></li></ul>

<ul><li><cite id="CITEREFSturm2017" class="citation journal cs1">Sturm, Thomas (2017). <a rel="nofollow" class="external text" href="https://doi.org/10.1007%2Fs11786-017-0319-z">"A Survey of Some Methods for Real Quantifier Elimination, Decision, and Satisfiability and Their Applications"</a>. Mathematics in Computer Science. 11 (3–4): 483–502. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1007%2Fs11786-017-0319-z">10.1007/s11786-017-0319-z</a>. <a href="Hdl_(identifier)" class="mw-redirect" title="Hdl (identifier)">hdl</a>:<a rel="nofollow" class="external text" href="https://hdl.handle.net/11858%2F00-001M-0000-002C-A3B5-B">11858/00-001M-0000-002C-A3B5-B</a>.</cite></li></ul>

</div></div><div><div class="zim-footer">

This article is issued from <a class="external text" title="Last edited on 2025-07-24" href="https://en.wikipedia.org/wiki/?title=Quantifier_elimination&oldid=1302350038">Wikipedia</a>. The text is available under <a class="external text" href="https://creativecommons.org/licenses/by-sa/4.0/deed.en">Creative Commons Attribution-Share Alike 4.0</a> unless otherwise noted. Additional terms may apply for the media files.

</div>

</div></div>

</div>

</main>

</div>

</body></html>